Section: New Results

Termination of Big Programs

Participants : Christophe Alias, Laure Gonnord, Guillaume Andrieu [Undergraduate Internship, Polytech'Lille] .

In a previous work with Alain Darte and Paul Feautrier, we showed how to prove the termination of a certain class of irregular programs with while loops  [29] . Our technique amounts to compute a sequential schedule – called ranking function – for the program, reinvesting most of the techniques from  [37] to schedule static loops. Our termination method is based on the resolution of a linear programming instance, and does not scale.

In most of big programs, all the information is not relevant for proving termination. Only a few slices need a termination proof. Moreover, inside a loop nest, termination can be proved incrementally. Inner loops are proved to terminate, and then are replaced by a summary. Our contribution is thus a reduction to prove a single loop termination, the price being the approximation made while computing the summary of a given (nest of) loop(s). This method can also be used to schedule irregular programs, which is clearly a need for program optimization.

A prototype has been designed and is currently under testing. A paper is in preparation. This method has been developed during the undergraduate internship of Guillaume Andrieu, from the Engineering School Polytech'Lille.